Step of Proof: inconsistent-bool-eq4 11,40

Inference at * 
Iof proof for Lemma inconsistent-bool-eq4:


  b:. ((b) = b False 
latex

 by ((D (0)
CollapseTHENA (Auto)
CollapseTHEN ((AutoBoolCase b
CollapseTHEN (((Try ((
CRWO "inconsistent-bool-eq" 0) 
CollapseTHEN (Auto)))
CollapseTHEN ((Try ((
CRWO "inconsistent-bool-eq2" 0) 
CollapseTHEN (Auto)))))) 
latex


C.


Definitionsleft + right, Unit, b, A, b, Void, , tt, ff, t  T, s = t, , x:AB(x), x:A  B(x), x:AB(x), P  Q, P & Q, P  Q, P  Q, False
Lemmaseqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, assert wf, bool wf, btrue wf, bfalse wf, inconsistent-bool-eq2, iff functionality wrt iff, inconsistent-bool-eq, false wf

origin